\begin{tabbing} (\=RW (AddrC [2;2] (UnfoldsC ``p{-}compose``)) 0) \+ \\[0ex]CollapseTHEN ((RepUR ``do{-}apply`` ( 0)$\cdot$) \\[0ex] \\[0ex]CollapseTHEN ((Fold `do{-}apply` 0) \\[0ex]CollapseTHEN (((if (0 \-\\[0ex])\= =0 then SplitOnConclITE else SplitOnHypITE (0))$\cdot$) \+ \\[0ex]CollapseTHENA (Auto$\cdot$)$\cdot$)$\cdot$)$\cdot$)$\cdot$ \- \end{tabbing}